The approaches described in this section are approaches that could be pursued, but not necessarily approaches that have been previously conceived or pursued. Therefore, unless otherwise indicated, it should not be assumed that any of the approaches described in this section qualify as prior art merely by virtue of their inclusion in this section.
Digital (discrete-time) systems are well known in the art. In general, the design and verification of digital systems involve the complex interrelationship among logical, arithmetic and timing dependencies in the system. In particular, the input and output dependencies of such systems are of special interest.
Techniques for verifying discrete-time systems include simulation, emulation, debugging and formal verification. Simulation verification is a software solution wherein a software algorithm is programmed to carry out the functions of the discrete-time system. Using the simulation software, a user is able to construct a software version of the digital system under consideration. The simulation software normally provides an output signal, typically in the form of a graphical waveform. Upon providing the input to the simulator, the user is able to observe the output from the waveform signal produced by the simulator.
Emulation is a hardware solution for verifying the designs of digital systems. Emulation commonly involves the use of FPGA (Field-Programmable Gate Array) devices, a type of logic chip that can be programmed. An FPGA is capable of supporting thousands of gates. A user is able to set the potential connections between the logic gates of the FPGA. Using FPGA devices, the user is able to prototype the digital system under consideration for verifying the input/output dependencies of the system.
Debugging generally involves manually implementing and running the system design. If any problems result during execution, the user reverts to a previous step of the design process to ascertain the source of the problem. Once the user has made the necessary changes to the system design, the user again attempts to execute the system design to ascertain if there are any additional problems, and the process is repeated again.
There are several disadvantages associated with these verification techniques. First, simulation, emulation and debugging techniques are not exhaustive. That is, these techniques are, in general, not capable of completely verifying that a system design meets the behavioral requirements that are expected of it. In addition, there is the problem of “opaqueness.” What a user gets from debugging, emulation and traditional simulation is a mass of data in the form of input vectors and output vectors, but there is no visibility into cause and effect. So a user faced with an anomalous output value must engage in a tedious and time consuming process to ferret out the cause(s) of that anomalous value.
Formal verification is another general approach to system verification. Three types of formal verification include (1) model checking, (2) theorem proving and (3) constraint-based analysis.
Model checking is popular within the research community but has not found widespread commercial use. That is primarily because a system is modeled as a finite-state machine, and this finite-state machine grows exponentially with the number of storage elements (flip flops). For example, a 10-flip-flop system requires a thousand (1,024) states, and a 20-flip-flop system requires a million (1,048,576) states. Since systems of practical interest often contain thousands of flip flops, “model-checking” approaches can be overwhelmed by the massive number of states.
Theorem proving is also popular within the research community, but—like model checking—has not found widespread commercial use. That is because the tools are not automated and require continual guidance by an expert in the field of theorem proving.
Constraint-based analysis as disclosed in U.S. Pat. No. 6,820,068 discloses a verification apparatus and method that is automated and also does not entail modeling a system as a finite-state machine, thereby avoiding the problems associated with the combinatorial explosion in states. However, U.S. Pat. No. 6,820,068 does not disclose an apparatus and method for automatically extracting the input/output (“black-box”) behavior of a system. Nor can it tell a system designer who is faced with an anomalous output why Signal S has Value V at Time T.
Accordingly, there is a need for a mechanism for: (1) automatically extracting the input/output (“black-box”) behavior of a system and (2) telling a system designer who is faced with an anomalous output why Signal S has Value V at Time T.